Inference at * 1 1 
Iof proof for Lemma eq int eq true elim sqequal:



1. i : 
2. j : 
3. (i = j) ~ tt
  i = j 

latex

 by (\p. let x, y = dest_sqequal (h (-1) p) in 
 by (\p(Assert (mk_equal_term bool_term y y) 

 by (\p(AsTHENL [(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
 ) inil_term); SqSubstAtAddr [2] x (-1) 
 ) inil_term); SqSubsTHENL [(Auto_aux (first_nat 1:n
 ) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term); Id]]) p) 

latex

 1: 

 1: 4. (i = j) = tt
 1:   i = j
 .

Definitions	t  T
Lemmas	btrue wf